(declare-const x47707__fresh Bool)
(declare-const x47752__fresh Bool)
(declare-fun skoX () Real)
(declare-fun skoY () Real)
(declare-fun l2 () Bool)
(declare-fun l3 () Bool)
(assert (let (($x58 x47752__fresh)) (let ((?x31 0.0)) (let ((?x15 skoY)) (let (($x51 x47752__fresh)) (let (($x52 x47752__fresh)) (and (<= (+ (* skoX (- skoX (+ (- 3600060000000000000000000.0) (* skoX (* skoX (- 3600060000.0)))))) skoX) 970000000000000000000000000000.0) x47752__fresh)))))))
(assert (let ((?x88 skoY)) (let (($x133 x47707__fresh)) (<= (* skoY skoY (+ (* skoX (+ 3600060000000000000000000.0 skoX (* 3600060000.0 (* skoX skoX)))) 1.0)) 0.0))))
(check-sat)
